feat(pyndakaas): add reflected operators for BoolExp, Formula, and Lit (#100)

* Allow creating BoolLinExps from list of vars/lits

* Fix the issue using `__radd__`

* Remove unnecessary constructor

* Add remaining reciprocal functions

* Add missing BoolLinExp operations

Author: hbierlee

crates/pyndakaas/python/tests/test_modelling.py

@@ -4,12 +4,16 @@
 def test_bool_lin():
     f = pindakaas.CNF()
     x, y, z = f.new_vars(3)
-    c = x + y - z + 2
-    assert str(c) == "-x₃ + x₂ + x₁ + 2"
-    c = sum([y, y, z], x)
-    assert str(c) == "x₃ + x₂ + x₂ + x₁"
+    assert str(x + 2) == "x₁ + 2", "__add__ incorrect"
+    assert str(2 + x) == "x₁ + 2", "__radd__ incorrect"
+    assert str(x - 2) == "x₁ + -2", "__sub__ incorrect"
+    assert str(2 * x) == "2*x₁", "__mul__ incorrect"
+    assert str(x * 2) == "2*x₁", "__rmul__ incorrect"
+    assert str(x + y - z + 2) == "-x₃ + x₂ + x₁ + 2"
+    c = sum([x, y, z])
+    assert str(c) == "x₃ + x₂ + x₁"
     c *= 2
-    assert str(c) == "2*x₃ + 2*x₂ + 2*x₂ + 2*x₁"
+    assert str(c) == "2*x₃ + 2*x₂ + 2*x₁"
     c = x + y + z
     d = c == 2
     assert str(d) == "x₃ + x₂ + x₁ == 2"
@@ -18,17 +22,43 @@ def test_bool_lin():
     d = c >= 2
     assert str(d) == "x₃ + x₂ + x₁ >= 2"
 
+def test_bool_lin_ops():
+    f = pindakaas.CNF()
+    x, y, z = f.new_vars(3)
+    f = x + y
+    g = x - z
+    assert str(f + 2) == "x₂ + x₁ + 2", "__add__ incorrect"
+    assert str(2 + f) == "x₂ + x₁ + 2", "__radd__ incorrect"
+    assert str(f + g) == "-x₃ + x₁ + x₂ + x₁", "__add__ incorrect"
+    assert str(f * 2) == "2*x₂ + 2*x₁", "__mul__ incorrect"
+    assert str(2 * f) == "2*x₂ + 2*x₁", "__rmul__ incorrect"
 
-def test_lit_ops():
+def test_formula_ops():
     f = pindakaas.CNF()
     x, y, z = f.new_vars(3)
-    a = ~x | ~y
-    assert str(a) == "¬x₁ ∨ ¬x₂"
-    b = y & z
-    assert str(b) == "x₂ ∧ x₃"
-    c = x ^ y
-    assert str(c) == "x₁ ⊻ x₂"
-    d = x ^ True
-    assert str(d) == "x₁ ⊻ true"
-    e = x == y
-    assert str(e) == "x₁ ≡ x₂"
+    f = x & y
+    g = x | z
+    assert str(f & True) == "x₁ ∧ x₂ ∧ true", "__and__ incorrect"
+    assert str(True & f) == "x₁ ∧ x₂ ∧ true", "__rand__ incorrect"
+    assert str(f & g) == "x₁ ∧ x₂ ∧ (x₁ ∨ x₃)", "__and__ incorrect"
+    assert str(f | True) == "(x₁ ∧ x₂) ∨ true", "__or__ incorrect"
+    assert str(True | f) == "(x₁ ∧ x₂) ∨ true", "__ror__ incorrect"
+    assert str(f | g) == "x₁ ∨ x₃ ∨ (x₁ ∧ x₂)", "__or__ incorrect"
+    assert str(f ^ True) == "(x₁ ∧ x₂) ⊻ true", "__xor__ incorrect"
+    assert str(True ^ f) == "(x₁ ∧ x₂) ⊻ true", "__rxor__ incorrect"
+    assert str(f ^ g) == "(x₁ ∧ x₂) ⊻ (x₁ ∨ x₃)", "__xor__ incorrect"
+
+def test_lit_ops():
+    f = pindakaas.CNF()
+    x, y = f.new_vars(2)
+    assert str(x & True) == "x₁ ∧ true", "__and__ incorrect"
+    assert str(True & x) == "x₁ ∧ true", "__rand__ incorrect"
+    assert str(x | True) == "x₁ ∨ true", "__or__ incorrect"
+    assert str(True | x) == "x₁ ∨ true", "__ror__ incorrect"
+    assert str(x ^ True) == "x₁ ⊻ true", "__xor__ incorrect"
+    assert str(True ^ x) == "x₁ ⊻ true", "__rxor__ incorrect"
+    assert str(~x | ~y) == "¬x₁ ∨ ¬x₂"
+    assert str(x & y) == "x₁ ∧ x₂"
+    assert str(x ^ y) == "x₁ ⊻ x₂"
+    assert str(x == y) == "x₁ ≡ x₂"
+

crates/pyndakaas/src/lib.rs

@@ -224,6 +224,10 @@ mod pindakaas {
 			res
 		}
 
+		fn __radd__(&self, other: BoolLinArg) -> Self {
+			self.__add__(other)
+		}
+
 		fn __eq__(&self, other: i64) -> BoolLinCon {
 			BoolLinCon(BaseBoolLinCon::new(
 				self.0.clone(),
@@ -274,6 +278,10 @@ mod pindakaas {
 			res
 		}
 
+		fn __rmul__(&self, other: i64) -> Self {
+			self.__mul__(other)
+		}
+
 		fn __neg__(&self) -> Self {
 			Self(-self.0.clone())
 		}
@@ -330,6 +338,10 @@ mod pindakaas {
 			Self(self.0.clone() & other.as_formula())
 		}
 
+		fn __rand__(&self, other: FormulaArg) -> Self {
+			self.__and__(other)
+		}
+
 		fn __eq__(&self, other: FormulaArg) -> Self {
 			use BaseFormula::*;
 
@@ -368,13 +380,21 @@ mod pindakaas {
 			Formula(self.0.clone() | other.as_formula())
 		}
 
+		fn __ror__(&self, other: FormulaArg) -> Self {
+			self.__or__(other)
+		}
+
 		fn __str__(&self) -> String {
 			self.0.to_string()
 		}
 
 		fn __xor__(&self, other: FormulaArg) -> Self {
 			Formula(self.0.clone() ^ other.as_formula())
 		}
+
+		fn __rxor__(&self, other: FormulaArg) -> Self {
+			self.__xor__(other)
+		}
 	}
 
 	impl FormulaArg {
@@ -407,10 +427,18 @@ mod pindakaas {
 			self.as_bool_lin_exp().__add__(other)
 		}
 
+		fn __radd__(&self, other: BoolLinArg) -> BoolLinExp {
+			self.__add__(other)
+		}
+
 		fn __and__(&self, other: FormulaArg) -> Formula {
 			Formula(self.as_formula()).__and__(other)
 		}
 
+		fn __rand__(&self, other: FormulaArg) -> Formula {
+			Formula(self.as_formula()).__and__(other)
+		}
+
 		fn __eq__(&self, other: FormulaArg) -> Formula {
 			Formula(self.as_formula()).__eq__(other)
 		}
@@ -443,6 +471,10 @@ mod pindakaas {
 			self.as_bool_lin_exp().__mul__(other)
 		}
 
+		fn __rmul__(&self, other: i64) -> BoolLinExp {
+			self.__mul__(other)
+		}
+
 		fn __ne__(&self, other: FormulaArg) -> Formula {
 			Formula(self.as_formula()).__ne__(other)
 		}
@@ -451,6 +483,10 @@ mod pindakaas {
 			Formula(self.as_formula()).__or__(other)
 		}
 
+		fn __ror__(&self, other: FormulaArg) -> Formula {
+			self.__or__(other)
+		}
+
 		fn __str__(&self) -> String {
 			self.0.to_string()
 		}
@@ -463,6 +499,10 @@ mod pindakaas {
 			Formula(self.as_formula()).__xor__(other)
 		}
 
+		fn __rxor__(&self, other: FormulaArg) -> Formula {
+			self.__xor__(other)
+		}
+
 		pub fn is_negated(&self) -> bool {
 			self.0.is_negated()
 		}